Inference at * 1 
Iof proof for Lemma equiv rel functionality wrt iff:



1. T : Type
2. T' : Type
3. E : TT
4. E' : T'T'
5. T = T'
6. x, y:T. E(x,y)  E'(x,y)
  EquivRel(T;x,y.E(x,y))  EquivRel(T';x,y.E'(x,y)) 

latex

 by (Repeat (Unfolds ``equiv_rel refl sym trans`` 0)) 

latex

 1: 

 1:   ((a:T. E(a,a)) & (a, b:T. E(a,b)  E(b,a)) & (a, b, c:T. E(a,b)  E(b,c)  E(a,c)))
 1:    ((a:T'. E'(a,a))
 1:    & (a, b:T'. E'(a,b)  E'(b,a))
 1:    & (a, b, c:T'. E'(a,b)  E'(b,c)  E'(a,c)))
 .

Definitions

Trans(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), EquivRel(T;x,y.E(x;y))